(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(assert (let ((e1 5))
(let ((e2 1))
(let ((e3 0))
(let ((e4 (* v0 (- e3))))
(let ((e5 (- v0 v0)))
(let ((e6 (/ e3 (- e1))))
(let ((e7 (- v0 e4)))
(let ((e8 (+ e7 e6)))
(let ((e9 (/ e3 (- e1))))
(let ((e10 (+ e7 e4)))
(let ((e11 (/ e2 e2)))
(let ((e12 (distinct e10 v0)))
(let ((e13 (distinct e4 e6)))
(let ((e14 (distinct e9 e9)))
(let ((e15 (< e11 e10)))
(let ((e16 (<= e9 e11)))
(let ((e17 (<= e11 e7)))
(let ((e18 (> e5 e11)))
(let ((e19 (>= e7 e9)))
(let ((e20 (>= v0 e10)))
(let ((e21 (> e6 e5)))
(let ((e22 (= e7 e11)))
(let ((e23 (<= e8 e8)))
(let ((e24 (ite e14 e5 e5)))
(let ((e25 (ite e19 e5 e4)))
(let ((e26 (ite e22 e25 e5)))
(let ((e27 (ite e15 e10 e9)))
(let ((e28 (ite e23 e4 e10)))
(let ((e29 (ite e12 e7 e5)))
(let ((e30 (ite e21 e6 e9)))
(let ((e31 (ite e20 e29 e29)))
(let ((e32 (ite e17 e27 e8)))
(let ((e33 (ite e22 e11 e28)))
(let ((e34 (ite e12 v0 e24)))
(let ((e35 (ite e14 e32 e33)))
(let ((e36 (ite e12 e31 e5)))
(let ((e37 (ite e13 e5 e4)))
(let ((e38 (ite e20 e11 e7)))
(let ((e39 (ite e16 e32 e30)))
(let ((e40 (ite e18 e39 e6)))
(let ((e41 (> v0 e26)))
(let ((e42 (> e6 e11)))
(let ((e43 (= e27 e28)))
(let ((e44 (= e8 v0)))
(let ((e45 (distinct e32 e39)))
(let ((e46 (> e9 e31)))
(let ((e47 (>= e26 e39)))
(let ((e48 (distinct v0 e25)))
(let ((e49 (> e30 e27)))
(let ((e50 (distinct e5 e6)))
(let ((e51 (= e33 e36)))
(let ((e52 (< e36 e37)))
(let ((e53 (distinct e24 e29)))
(let ((e54 (< e35 e33)))
(let ((e55 (<= e36 e35)))
(let ((e56 (<= e32 e30)))
(let ((e57 (= e30 e6)))
(let ((e58 (distinct e11 e32)))
(let ((e59 (<= e40 e24)))
(let ((e60 (< e25 e8)))
(let ((e61 (distinct e26 e35)))
(let ((e62 (= e7 e36)))
(let ((e63 (= e31 e38)))
(let ((e64 (distinct e39 v0)))
(let ((e65 (< v0 e11)))
(let ((e66 (> e5 v0)))
(let ((e67 (<= e7 e36)))
(let ((e68 (> e4 e29)))
(let ((e69 (<= e9 e28)))
(let ((e70 (distinct e5 e24)))
(let ((e71 (distinct e6 e35)))
(let ((e72 (< e10 e38)))
(let ((e73 (< e29 e25)))
(let ((e74 (>= e37 e29)))
(let ((e75 (distinct e7 e4)))
(let ((e76 (< e4 e26)))
(let ((e77 (< e25 e8)))
(let ((e78 (< e4 e27)))
(let ((e79 (< e38 e32)))
(let ((e80 (<= e38 e31)))
(let ((e81 (= e6 e6)))
(let ((e82 (>= e36 e8)))
(let ((e83 (distinct e8 e26)))
(let ((e84 (= e36 e10)))
(let ((e85 (= e35 e35)))
(let ((e86 (distinct e27 e28)))
(let ((e87 (<= e6 e11)))
(let ((e88 (>= e34 e30)))
(let ((e89 (not e87)))
(let ((e90 (not e45)))
(let ((e91 (not e64)))
(let ((e92 (or e77 e13)))
(let ((e93 (=> e92 e91)))
(let ((e94 (xor e72 e19)))
(let ((e95 (ite e75 e94 e88)))
(let ((e96 (and e84 e49)))
(let ((e97 (and e66 e78)))
(let ((e98 (not e41)))
(let ((e99 (xor e90 e22)))
(let ((e100 (xor e15 e16)))
(let ((e101 (not e89)))
(let ((e102 (and e83 e56)))
(let ((e103 (=> e53 e20)))
(let ((e104 (or e98 e81)))
(let ((e105 (ite e18 e42 e80)))
(let ((e106 (ite e85 e96 e105)))
(let ((e107 (not e62)))
(let ((e108 (not e14)))
(let ((e109 (or e55 e43)))
(let ((e110 (= e61 e17)))
(let ((e111 (xor e106 e54)))
(let ((e112 (=> e57 e69)))
(let ((e113 (= e58 e76)))
(let ((e114 (not e108)))
(let ((e115 (= e59 e97)))
(let ((e116 (=> e63 e48)))
(let ((e117 (xor e70 e101)))
(let ((e118 (or e103 e111)))
(let ((e119 (xor e12 e60)))
(let ((e120 (not e117)))
(let ((e121 (xor e65 e44)))
(let ((e122 (not e115)))
(let ((e123 (ite e79 e121 e68)))
(let ((e124 (xor e120 e112)))
(let ((e125 (and e100 e99)))
(let ((e126 (not e113)))
(let ((e127 (=> e123 e110)))
(let ((e128 (and e109 e67)))
(let ((e129 (=> e23 e124)))
(let ((e130 (not e129)))
(let ((e131 (= e46 e47)))
(let ((e132 (or e74 e130)))
(let ((e133 (ite e118 e86 e82)))
(let ((e134 (ite e131 e116 e114)))
(let ((e135 (and e127 e93)))
(let ((e136 (xor e128 e71)))
(let ((e137 (ite e133 e104 e73)))
(let ((e138 (xor e134 e122)))
(let ((e139 (=> e137 e51)))
(let ((e140 (and e136 e132)))
(let ((e141 (xor e135 e138)))
(let ((e142 (xor e125 e95)))
(let ((e143 (= e50 e107)))
(let ((e144 (and e143 e102)))
(let ((e145 (not e52)))
(let ((e146 (or e145 e145)))
(let ((e147 (and e144 e140)))
(let ((e148 (xor e142 e142)))
(let ((e149 (not e146)))
(let ((e150 (xor e126 e149)))
(let ((e151 (=> e21 e147)))
(let ((e152 (= e150 e141)))
(let ((e153 (= e152 e148)))
(let ((e154 (=> e153 e139)))
(let ((e155 (ite e151 e154 e151)))
(let ((e156 (not e155)))
(let ((e157 (and e119 e156)))
e157
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
